R:Realizer. (R-size(R)  1)  R-Feasible(R)  ([[R]]  Dsys) 

latex

Definitions

ff, Rplus?(x1), Rnone?(x1), b, if b then t else f fi , A c B, A, @i: A, , case(R)Rnone: noneleft  right: comb(left;right)base(b). base(b), P & Q, True, x. t(x), [[R]], Dsys, t  T, R-Feasible(R), R-size(R), P  Q, x:A. B(x), False, , x(s), Unit, Realizer, left  right, , Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), Rnone(),

Lemmas

R-base-ma wf, msga wf, R-loc wf, eq id wf, ifthenelse wf, false wf, es realizer wf, Rrframe wf, Rbframe wf, Raframe wf, Rpre wf, Rsends wf, Reffect wf, Rsframe wf, Rframe wf, Rinit wf, nat plus wf, Rplus wf, R-size wf, le wf, Rnone wf, R-Feasible wf, ma-empty wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf